Nuprl Lemma : R-size-implies
11,40
postcript
pdf
R
:Realizer.
(1 < R-size(
R
))
(
A
,
B
:Realizer. (
R
= (
A
B
) & (R-size(
A
) < R-size(
R
)) & (R-size(
B
) < R-size(
R
))))
latex
Definitions
x
,
y
,
z
,
w
,
v
.
t
(
x
;
y
;
z
;
w
;
v
)
,
x
,
y
,
z
,
u
,
v
,
w
.
t
(
x
;
y
;
z
;
u
;
v
;
w
)
,
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
,
y
,
z
,
w
.
t
(
x
;
y
;
z
;
w
)
,
t
T
,
x
.
t
(
x
)
,
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
R-size(
R
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
x
(
s1
,
s2
,
s3
,
s4
,
s5
)
,
x
(
a
,
b
,
c
,
d
,
e
,
f
)
,
x
(
s1
,
s2
,
s3
)
,
x
(
s1
,
s2
,
s3
,
s4
)
,
{
T
}
,
x
(
s
)
Lemmas
nat
plus
wf
,
R-size
wf
,
Rplus
wf
,
finite-prob-space
wf
,
bool
wf
,
fpf
wf
,
decl-type
wf
,
decl-state
wf
,
IdLnk
wf
,
Knd
wf
,
Id
wf
,
rationals
wf
,
es
realizer
wf
,
es
realizer
ind
wf
,
es
realizer-induction
origin
R:Realizer.
(
A,B:Realizer. (R = (A 
B) & (R-size(A) < R-size(R)) & (R-size(B) < R-size(R)))) R:Realizer.
(A,B:Realizer. (R = (A B) & (R-size(A) < R-size(R)) & (R-size(B) < R-size(R)))) 
x,y,z,w,v. t(x;y;z;w;v)
T
